$\forall$$A$:Type$_{\mbox{\scriptsize i}}$. discrete\_struct\{i:l\}($A$) $\in$ Type$_{\mbox{\scriptsize i'}}$